|
First-order logic is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. It is also known as first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic. First-order logic uses quantified variables over (non-logical) objects. This distinguishes it from propositional logic, which does not use quantifiers. A theory about some topic is usually a first-order logic together with a specified domain of discourse over which the quantified variables range, finitely many functions from that domain to itself, finitely many predicates defined on that domain, and a set of axioms believed to hold for those things. Sometimes "theory" is understood in a more formal sense, which is just a set of sentences in first-order logic. The adjective "first-order" distinguishes first-order logic from higher-order logic in which there are predicates having predicates or functions as arguments, or in which one or both of predicate quantifiers or function quantifiers are permitted. In first-order theories, predicates are often associated with sets. In interpreted higher-order theories, predicates may be interpreted as sets of sets. There are many deductive systems for first-order logic which are both sound (all provable statements are true in all models) and complete (all statements which are true in all models are provable). Although the logical consequence relation is only semidecidable, much progress has been made in automated theorem proving in first-order logic. First-order logic also satisfies several metalogical theorems that make it amenable to analysis in proof theory, such as the Löwenheim–Skolem theorem and the compactness theorem. First-order logic is the standard for the formalization of mathematics into axioms and is studied in the foundations of mathematics. Peano arithmetic and Zermelo–Fraenkel set theory are axiomatizations of number theory and set theory, respectively, into first-order logic. No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the natural numbers or the real line. Axioms systems that do fully describe these two structures (that is, categorical axiom systems) can be obtained in stronger logics such as second-order logic. For a history of first-order logic and how it came to dominate formal logic, see José Ferreirós (2001). ==Introduction== While propositional logic deals with simple declarative propositions, first-order logic additionally covers predicates and quantification. A predicate takes an entity or entities in the domain of discourse as input and outputs either True or False. Consider the two sentences "Socrates is a philosopher" and "Plato is a philosopher". In propositional logic, these sentences are viewed as being unrelated and might be denoted, for example, by variables such as ''p'' and ''q''. The predicate "is a philosopher" occurs in both sentences, which have a common structure of "''a'' is a philosopher". The variable ''a'' is instantiated as "Socrates" in the first sentence and is instantiated as "Plato" in the second sentence. The use of predicates, such as "is a philosopher" in this example, distinguishes first-order logic from propositional logic. Relationships between predicates can be stated using logical connectives. Consider, for example, the first-order formula "if ''a'' is a philosopher, then ''a'' is a scholar". This formula is a conditional statement with "''a'' is a philosopher" as its hypothesis and "''a'' is a scholar" as its conclusion. The truth of this formula depends on which object is denoted by ''a'', and on the interpretations of the predicates "is a philosopher" and "is a scholar". Quantifiers can be applied to variables in a formula. The variable ''a'' in the previous formula can be universally quantified, for instance, with the first-order sentence "For every ''a'', if ''a'' is a philosopher, then ''a'' is a scholar". The universal quantifier "for every" in this sentence expresses the idea that the claim "if ''a'' is a philosopher, then ''a'' is a scholar" holds for ''all'' choices of ''a''. The ''negation'' of the sentence "For every ''a'', if ''a'' is a philosopher, then ''a'' is a scholar" is logically equivalent to the sentence "There exists ''a'' such that ''a'' is a philosopher and ''a'' is not a scholar". The existential quantifier "there exists" expresses the idea that the claim "''a'' is a philosopher and ''a'' is not a scholar" holds for ''some'' choice of ''a''. The predicates "is a philosopher" and "is a scholar" each take a single variable. In general, predicates can take several variables. In the first-order sentence "Socrates is the teacher of Plato", the predicate "is the teacher of" takes two variables. An interpretation (or model) of a first-order formula specifies what each predicate means and the entities that can instantiate the variables. These entities form the domain of discourse or universe, which is usually required to be a nonempty set. For example, in interpretation with the domain of discourse consisting of all human beings and the predicate "is a philosopher" understood as "was the author of the''Republic''", the sentence "There exists ''a'' such that ''a'' is a philosopher" is seen as being true, as witnessed by Plato. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「First-order logic」の詳細全文を読む スポンサード リンク
|